COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\batchmode
C00013 00003	\def\Lemma:{\par\noindent{\bf Lemma:}\quad}
C00015 00004	\prob {1.1}.
C00020 00005	\prob{1.2}. The functions |istail| and |commontail| are defined as:
C00023 00006	\prob{1.4}. This turned out to be one of the hardest problems.  Here is a fairly
C00030 00007	\prob {1.5}.  First, define
C00037 ENDMK
C⊗;
\batchmode
\def\prob#1{{\bf Problem #1}\par}
\magnification = \magstephalf
\catcode`|=13
\def|#1|{\hbox{\it#1\/}}
\parindent 0pt
\parskip 0pt
\def\pskip{\penalty-1000\vskip 6pt plus 2pt minus 1pt}
\def\ppskip{\penalty-2000\vskip 10pt plus 3pt minus 2pt}
\def\no(#1){\noindent\hbox to 6em{(#1)\hfill}}
\catcode`⊗=13
\def⊗{\hbox to 2em{}}
\def\IF{\mathop{\hbox{\bf if}}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}
\def\AND{\mathrel{\bf and}}
\def\OR{\mathrel{\bf or}}
\def\NOT{\mathop{\hbox{\bf not}}}
\def\N{\mathop{\hbox{\bf n}}}
\def\T{\hbox{\tt T}}
\def\NIL{\hbox{\tt NIL}}
\def\.{\mathbin{.}}
\def\A{\mathop{\hbox{\bf a}}}
\def\D{\mathop{\hbox{\bf d}}}
\def\EQ{\mathrel{\bf eq}}
\def\AT{\mathop{\hbox{\bf at}}}
\def\quote#1{\hbox{\sfcode`.=1000\tt#1}}
\def\list#1{\langle#1\rangle}
\def\xskip{\hskip7pt plus3pt minus4pt}

{\catcode`\↑↑M=13\global\let ↑↑M=\linebreak}	% This must be on one line!
\def\lines{\par\groupbegin
	\catcode`\ =12
	\sfcode`.=1000
	\parindent 0pt
	\leftskip 25pt
	\rightskip 0pt plus 1fil
	\interlinepenalty 50
	\baselineskip 12pt
	\parskip 12pt plus 6pt minus 6pt
	\catcode`\↑↑M=13
	\tt\eat}
\def\eat#1{}					% to eat the first <cr>
\def\endlines{\par\vskip\minusthe\baselineskip	% cancel the last empty line
	\vskip\the\parskip			% put in space
	\groupend\vskip\minusthe\parskip}	% cancel the next space to go in

\centerline{CS 206---Recursive Programming and Proving}
\centerline{Homework 3,4 Solutions}
\centerline{Tuesday, November 22, 1983}

\ppskip
\def\Lemma:{\par\noindent{\bf Lemma:}\quad}
\def\Theorem:{\par\noindent{\bf Theorem:}\quad}
\def\Proof:{\par\noindent{\bf Proof:}\quad}
\def\samelength{\mathop{\it samelength}}
\def\reverse{\mathop{\it reverse}}
\def\length{\mathop{\it length}}
\def\istail{\mathop{\it istail}}
\def\com{\mathop{\it commontail}}
\def\upto{\mathop{\it upto}}


\ppskip
\prob {1.1}.
There were two basic approaches to solving this problem, differing
in whether the formula $∀u.\,\samelength[u,\reverse u]$ was proved directly
or whether |length| was used as an auxiliary function.  The functions used
are defined as follows:
\pskip
$⊗⊗⊗\reverse u←\IF\N u\THEN\NIL\ELSE\reverse[\D u]*\list{\A u}$\par
\pskip
$⊗⊗⊗\samelength[u,v]←$\par
$⊗⊗⊗⊗\IF\N u\OR\N v\THEN\N u\AND\N v$\par
$⊗⊗⊗⊗\ELSE\samelength[\D u,\D v]$\par
\pskip
$⊗⊗⊗\length u←\IF\N u\THEN 0\ELSE 1+\length \D u$\par
\pskip
\noindent Here is a direct proof :
\pskip
\Lemma: $∀x\,u\,v.\,\samelength[u,v*\list{x}]≡\samelength[u,x\.v]$.
\Proof: We will prove the lemma by list induction on $\Phi(v)$:
$∀x\,u.\,\samelength[u,v*\list{x}]≡\samelength[u,x\.v]$.
First, $\Phi(\NIL)$ is $∀x\,u.\,\samelength[u,\list{x}]≡
\samelength[u,x\.\NIL]$ (expanding the |append| on the left-hand side),
which is valid since $\list{x}=x\.\NIL$ for any $x$.
Now, assume $\Phi(v)$ as an inductive hypothesis; then $\Phi(y\.v)$ is
$∀x\,u.\,\samelength[u,(y\.v)*\list{x}]≡\samelength[u,x\.(y\.v)]$.
If $u=\NIL$, both sides of the equivalence are \NIL\ using the definition
of |samelength| and facts about |cons| and |append|; and if $u≠\NIL$,
the formula simplifies to $\samelength[\D u,v*\list{x}]≡\samelength[\D u,y\.v]$.
Using the inductive hypothesis, this is the same as
$\samelength[\D u,x\.v]≡\samelength[\D u,y\.v]$, but here again the second
argument to both calls of |samelength| is non-\NIL; so either $\D u=\NIL$ and
both sides are false, or $\D u≠\NIL$ and then the formula becomes
$\samelength[\D\D u,v]≡\samelength[\D\D u,v]$, which is valid.
\pskip
\Theorem: $∀u.\,\samelength[u,\reverse u]$.
\Proof: By induction on $\Phi(u)$: $\samelength[u,\reverse u]$.
$\Phi(\NIL)$ is trivial (apply the definitions of |reverse| and |samelength|).
Assuming $\Phi(u)$, $\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\samelength[x\.u,\reverse [x\.u]]$\par
$⊗⊗⊗⊗≡\samelength[x\.u,\reverse u*\list{x}]$\par
$⊗⊗⊗⊗≡\samelength[x\.u,x\.\reverse u]$\hskip 3em (by the lemma)\par
$⊗⊗⊗⊗≡\samelength[u,\reverse u]$\par
\pskip
and the last line is true by the inductive hypothesis.

\ppskip
A proof using |length| as an auxiliary function would prove the following
lemmas, from which the main result follows.
\pskip
\Lemma: $∀u\,v.\,\samelength[u,v]≡\length u=\length v$.
\Lemma: $∀u\,v.\,\length[u*v]=\length u+\length v$.
\pskip
Both of these can be proved by list induction on $u$ or $v$ (or both).

\ppskip
\prob{1.2}. The functions |istail| and |commontail| are defined as:
\pskip
$⊗⊗⊗\istail[u,v]←u=v\OR[\NOT\N v\AND\istail[u,\D v]]$\par
\pskip
$⊗⊗⊗\com[u,v]←\IF\istail[u,v]\THEN u\ELSE\com[\D u,v]$\par
\pskip
Let $\Phi(u)$ be $\istail[\com[u,v],v]$.  Then $\Phi(\NIL)$ is
seen to be true by applying the function definitions, and assuming $\Phi(u)$,
$\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\istail[\com[x\.u,v],v]$\par
$⊗⊗⊗⊗≡\istail[\IF\istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],v]$\par
$⊗⊗⊗⊗≡\IF\istail[x\.u,v]\THEN\istail[x\.u,v]\ELSE\istail[\com[u,v],v]$\par
\pskip
which is valid, applying the inductive hypothesis.  Since no assumptions were
made about $x$, we can quantify over $x$, completing the inductive step.

\ppskip
\prob{1.3}. Let $\Phi(u)$ be $\istail[\com[u,v],u]$.  Again $\Phi(\NIL)$
is easy to prove by applying the definitions, and assuming $\Phi(u)$ as an
inductive hypothesis, $\Phi(x\.u)$ is
\pskip
$⊗⊗⊗\istail[\com[x\.u,v],x\.u]$\par
$⊗⊗⊗⊗≡\istail[\IF\istail[x\.u,v]\THEN x\.u\ELSE\com[u,v],x\.u]$\par
$⊗⊗⊗⊗≡\IF\istail[x\.u,v]\THEN\istail[x\.u,x\.u]\ELSE\istail[\com[u,v],x\.u]$\par
\pskip
If $\istail[x\.u,v]$ holds, then this becomes true since $\istail[x\.u,x\.u]$.
Otherwise, we get
\pskip
$⊗⊗⊗\istail[\com[u,v],x\.u]$\par
$⊗⊗⊗⊗≡\com[u,v]=x\.u\OR[\NOT\N[x\.u]\AND\istail[\com[u,v],u]]$\par
\pskip
which becomes true by using the inductive hypothesis.

\ppskip
\prob{1.4}. This turned out to be one of the hardest problems.  Here is a fairly
simple proof.  First, some lemmas.
\pskip
\noindent {\bf Lemma 1:}\quad $∀u.\,\istail[\NIL,u]$.
\Proof: Straightforward induction on $u$.
\pskip
\noindent {\bf Lemma 2:}\quad (a) $∀u.\,\com[\NIL,u]=\NIL$.\par
$⊗⊗$(b) $∀u.,\com[u,\NIL]=\NIL$.\par
\Proof: (a) Simple consequence of Lemma 1 and definition of |commontail|.\par
$⊗⊗$(b) Induction on $u$.
\pskip
\noindent {\bf Lemma 3:}\quad
$∀u\,v.\,\istail[u,v]⊃\length u≤\length v$.\par
\Proof: Let $\Phi(v)$ be $∀u.\,\istail[u,v]⊃\length u≤\length v$.
$\Phi(\NIL)$ simplifies to $∀u.\,\istail[u,\NIL]⊃\length u≤0$, and
$\istail[u,\NIL]$ simplifies to $u=\NIL$.  Therefore $\Phi(\NIL)$ is valid.
Assuming $\NOT\N v$ and $\Phi(\D v)$, $\Phi(v)$ becomes
$∀u.\,u=v\OR\istail[u,\D v]⊃\length u≤\length v$.  The case $u=v$ reduces
to true immediately, and the case $\istail[u,\D v]$ implies
$\length u≤\length \D v$, from which $\length u≤\length v$ follows
easily.  This completes the inductive step, and the proof of this lemma.
\pskip
Lemma 3 is used here only to prove Lemma 4,
but could be used much more in a completely different approach to
this set of problems.
\pskip
\noindent {\bf Lemma 4:}\quad $∀u\,v.\,\istail[u,v]\AND\istail[v,u]⊃u=v$.
\Proof: If $u=v$, the implication follows immediately.  So assume $u≠v$.
If $u=\NIL$ and $v≠\NIL$ then $\istail[v,u]$ is false, and we are done.
Similarly if $v=\NIL$ and $u≠\NIL$ then $\istail[u,v]$ must be false.
Finally, if $u≠\NIL$ and $v≠\NIL$, and if $\istail[u,v]\AND\istail[v,u]$,
then both $\istail[u,\D v]$ and $\istail[v,\D u]$ are true from the
definition of |istail|, because $u≠v$.  By
the previous lemma, this means that $\length u≤\length \D v$ and
$\length v≤\length \D u$.  But then it is easy to show that
$\length u<\length v$ and $\length v<\length u$, which contradicts
axioms about the natural numbers, so the left side of the implication must
be false.  Since we have now taken care of all possible cases involving
$u$ and $v$, we can insert the $∀u\,v$ quantifier, and the lemma is proved.
\pskip
Finally, we come to the proof of the main result.
\pskip
\Theorem: $∀u\,v.\,\com[u,v]=\com[v,u]$.
\Proof: The trick is to prove the following formula:
$$∀u\,v\,w.\,\istail[w,u]\AND\istail[w,v]⊃\istail[w,\com[u,v]].$$
This expresses the fact that the |commontail| of $u$ and $v$ is the largest
list that is a tail of both $u$ and $v$.  Now, we prove this formula by
induction on $u$.  $\Phi(\NIL)$ is easy, as usual, because the right side
of the implication simplifies to true using Lemmas 1 and 2.
Assuming $\Phi(u)$, we can write out $\Phi(x\.u)$ as
\pskip
$⊗⊗⊗∀v\,w.\,\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,\com[x\.u,v]]$\par
$⊗⊗⊗⊗≡∀v\,w.\,\IF\istail[x\.u,v]\THEN\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,x\.u]$\par
$⊗⊗⊗⊗⊗\ELSE\istail[w,x\.u]\AND\istail[w,v]⊃\istail[w,\com[u,v]]$\par
$⊗⊗⊗⊗≡∀v\,w.\,\NOT\istail[x\.u,v]\AND\istail[w,x\.u]\AND\istail[w,v]⊃\null$\par
$⊗⊗⊗⊗⊗⊗⊗\istail[w,\com[u,v]]$\par
\pskip
In the last line above, the $\THEN$ part of the conditional was seen to be
true from the condition, so the expression could be simplified.  Now,
$\istail[w,x\.u]$ allows us to split into the two cases $w=x\.u$ and
$\istail[w,u]$.  In the first case, $\istail[w,v]$ becomes $\istail[x\.u,v]$,
but we already have the negation of this as part of the same conjunction,
so the left side of the implication is false.  Otherwise, from $\istail[w,u]$
and $\istail[w,v]$, we can derive $\istail[w,\com[u,v]]$ by the inductive
hypothesis, so we are done.  Thus the inductive step is complete.
\pskip
Finally, we use the fact just proved with $w=\com[v,u]$.  Then
$\istail[w,u]$ and $\istail[w,v]$ are the statements proved in problems 1.2
and 1.3, so we can deduce $\istail[w,\com[u,v]]$, that is,
$\istail[\com[v,u],\com[u,v]]$.  By an argument symmetric to the one just
given, we can show that $\istail[\com[u,v],\com[v,u]]$.  Then, applying
Lemma 4, we get the desired final result.

\ppskip
\prob {1.5}.  First, define
\pskip
$⊗⊗⊗\upto[u,v]←\IF u=v\THEN\NIL\ELSE\A v\.\upto[u,\D v]$.\par
\pskip
\Lemma: $∀u\,v.\,\istail[u,v]⊃\upto[u,v]*u=v$.
\Proof: Let $\Phi(v)$ be $∀u.\,\istail[u,v]⊃\upto[u,v]*u=v$.  Then $\Phi(\NIL)$
is $∀u.\,\istail(u,\NIL)⊃\upto[u,\NIL]*u=\NIL$.  Now, if $\istail[u,\NIL]$ then
we must have $u=\NIL$ in order to satisfy the definition of |istail|.  Then
$\upto[u,\NIL]*u=\NIL$ is true by applying the definition of |upto|.  For the
inductive step, assume $\Phi(v)$; then $\Phi(x\.v)$ is
$∀u.\,\istail[u,x\.v]⊃\upto[u,x\.v]*u=x\.v$.  There are two cases: $u=x\.v$
or $u≠x\.v$.  If $u=x\.v$, the formula is made true by simplifying and applying
definitions.  Otherwise, it becomes $\istail[u,v]⊃x\.\upto[u,v]*u=x\.v$.
Using the inductive hypothesis, is $\istail[u,v]$, then $\upto[u,v]*u=v$, so
the right side of the implication becomes $x\.v=x\.v$, and the formula is
proved.
\pskip
From this Lemma and problem 1.2, the statement of problem 1.5 follows
immediately.

\ppskip
\prob{1.6}.  This follows immediately from the Lemma above and problem 1.3.
Alternately, it follows immediately from probles 1.5 and 1.6.
\ppskip

\vfill\end